^e
例
code:alloy
sig Node {
edge: set Node
}
上記のようなsigに対し、n: Nodeで、n.edgeと書くと、
n自体が接続しているNodeの集合のみを表す
そこから更に、n.edge.edgeとかn.edge.edge.edgeみたいに、延々に参照されるもの全てを指定したい時、n.^edgeと書けば良い
ただし、この時、推移的に到達可能でなければn自身は含まれない
n.edge.edge.edge == nだったりするなら含むが、ということmrsekut.icon
常に自身も含めるなら反射律も足した*eを使えば良い 例
code:alloy
pred noSelfLoop {
no c: Composite | c in c.^children
}
Compositeの循環参照がないことを表す述語
「「cからchildrenを辿って到達可能なComponenの中に自身を含むようなc」が存在しない」
^r = r + r.r + r.r.r + ...